Inference at * 1 1 2 1 
Iof proof for Lemma dcdr-to-bool-equivalence:



1. P : 
2. P
3. (inr  )
  P 

latex

 by ((Unfold `assert` ( -1)) 
CollapseTHEN (Reduce (-1))) 
CollapseTHEN (Trivial) 

latex

C.

Definitions

b, False